Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

So und zwar geht es heute noch mal um Algorithmik. Also wie designen wir

Entscheidungsprozeduren für Logik erster Stufe.

So wir können jetzt hier nicht zeigen. Es ist aber nicht fürchterlich schwer

gegeben, Kenntnis gewisser unentscheidbarer Probleme, die man sich

anderswo einsammelt, dass Gültigkeit oder auch Erfüllbarkeit, das ist egal, in

Logik erster Stufe, also Prädikatenlogik erster Stufe, im Allgemeinen

unentscheidbar ist. Deswegen hatten wir halt auch beim

Resolutionsalgorithmus für Prädikatenlogik, also anders als bei dem für

Haushagenlogik, beobachtet, dass der zwar richtige Antworten gibt, wenn er

terminiert, aber eventuell eben nicht terminiert.

Das gilt aber links erstmal nur für Aussagenlogik schlechthin, also wenn ich

die Frage stelle, gegeben irgendeine Quatsch nicht Aussagenlogik, Prädikatenlogik, wenn

ich die auch Frage stelle, gegeben irgendeine Prädikatenlogische Formel, ist

die erfüllbar oder gültig? Das ist Modulonegation, dieselbe Frage ist nachher.

Das ist unentscheidbar. Wenn ich aber die Welt, in der ich lebe, einschränke und also

gewisser Art sage, ich rede über konkretere Strukturen, die ich irgendwie

akkussomatisieren, dann kann es passieren, mit sehr viel Glück, dass die Frage der

Erfüllbarkeit einer Formel über dieser Theorie wieder entscheidbar wird.

Das definieren wir einmal formal durch.

Das ist übrigens, fangen wir schon mal an, das ist im Skript Kapitel 9.

So, wir definieren jetzt also erstmal, was eine Theorie ist. Das ist mehr oder weniger

implizit und zumindest in den Übungsaufgaben auch schon dran gewesen.

Eine Theorie ist zunächst mal ein Ta, Sigma, Phi. Wir schreiben die Theorie selber mit

typischen Buchstaben, schön T oder sowas.

So, und diese beiden Teile des Paares sind also erstens eine Signatur, also eine

Ansammlung von Symbolen, die mir sagen, worüber ich überhaupt rede. So, das eine

habe ich schon jetzt nicht beachtet, ich schreibe also jetzt weiter rechts hier.

Und eine Menge Sigma, Quatsch, eine Menge Phi von Formeln und zwar eben von Sigma-

Formeln, das heißt die Menge von Formeln, die da steht, die soll zu der angegebene

Signatur passen. So, dann, gut, das ist das, was man so denkt, also typisches

Beispiel, was weiß ich, Piano-Arithmetik. Wir haben eine Signatur, Null und

Nachfolger und die Axiome der Piano-Arithmetik. So, und jetzt definieren wir,

dass ein Modell einer Theorie ist, das ist auch relativ klar.

Das ist zunächst also mal einmal ein Modell dieser Signatur, also ein Sigma-Modell,

aber eben eins mit bestimmten Eigenschaften, naja eben ein Modell, das eben

all die, ach so, Moment, wir insistieren, dass das Sätze sind, also geschlossene

Formeln und dann können wir vereinfacht schreiben, also wir brauchen jetzt nicht

mehr über Umgebung zu reden, sondern wir können vereinfacht schreiben, das Modell

erfüllt all diese Sätze, weil das geschlossene Formeln sind, kommt es auf

die Umgebung nicht an.

So, die Kinder, die haben noch Namen, das sind die Axiome der Theorie.

So, und jetzt definieren wir Erfüllbarkeit über T, also nicht mehr

Erfüllbarkeit schlechthin, sondern Erfüllbarkeit über T. So, und wir sagen,

eine Formel sei erfüllbar über T, naja, können Sie sich was ausrechnen, ja, also

vorher hieß Erfüllbar, es existiert ein Modell, das psi erfüllt.

So, und jetzt verlangen wir stattdessen Existenz eben eines T-Modells, das psi

erfüllt. Ja, jetzt sind wir mal etwas exakter hier.

So, ich will jetzt hier nicht darauf einschränken, dass das psi ein Satz ist,

sondern das psi kann eine Formel sein. So, und ich sage, das psi ist erfüllbar